COMMENT ⊗   VALID 00002 PAGES
C REC  PAGE   DESCRIPTION
C00001 00001
C00002 00002	
C00006 ENDMK
C⊗;

subst[x;y;z] <= 
	[atom[z] → [eq[y;z] → x; T → z];
	 T → cons[subst[x;y;car[z]];subst[x;y;cdr[z]]] ]


      _____________    __________________   ________________ 
subst[car[(A . NIL)]; [eq[A;T] → B; T → B]; ((B . 1).(C . B))]

			= subst[A;B;((B . 1) . (C . B))] 



subst[A;B;((B . 1) . (C . B))] = 
	[atom[((B . 1).(C. B))] → [eq[B;((B . 1).(C . B))] → B; T → ((B . 1).(C . B))];
	 T → cons[subst[A;B;car[((B . 1).(C . B))]];
		  subst[A;B;cdr[((B . 1).(C . B))]]] ]

***NOTES***
1. when we get to the machine, the evaluation scheme will NOT explicitly
substitute the values for the variables in the body of the function;
however the logical effect is the same.

2. note that after the substution of values for variables is made, ther are lots
of expresssions which, if evaluated, would result in "undefined".
For example "eq[B;((B . 1).(C . B))]" would lose if we evaluated it.
But notice that the above expression  is biased by the test for atom-ness, and
we will NOT evaluated eq[B;((B . 1).(C . B))]!!! 

Thus after some simplifications:

subst[A;B;((B . 1) . (C . B))] = 
	     cons[subst[A;B;car[((B . 1).(C . B))]];
		  subst[A;B;cdr[((B . 1).(C . B))]]] 

      =	     cons[subst[A;B;(B . 1)];
		  subst[A;B;(C . B)]] 

applying the definition of subst, ans simplifying:

      =	     cons[cons[subst[A;B;car[(B . 1)]]; subst[A;B;cdr[(B . 1)]]]
		  subst[A;B;(C . B)]] 

      =	     cons[cons[subst[A;B;car[(B . 1)]]; subst[A;B;cdr[(B . 1)]]]
		  cons[subst[A;B;car[(C . B)]]; subst[A;B;cdr[(C . B)]]]]

      =	     cons[cons[subst[A;B;B]; subst[A;B;1]]
		  cons[subst[A;B;C]; subst[A;B;B]]]

going to the definition again, we simplify to:

      =	     cons[cons[A;1];
		  cons[subst[A;B;C]; subst[A;B;B]]]

      =	     cons[cons[A;1];
		  cons[C;A]]

      =	     cons[(A . 1);
		  (C . A)]


      =   ((A . 1).(C . A))      SIGH!!!!

Problem: 

evaluate   subst[cons[A;NIL]; cdr[(B . Y)]; ((A . Y).(Y .(U . W)))]

NOTICE: y is a variable; Y is an atom, therefore an S-expr!!!